//  Copyright 2011 Charlie Garrett
//
//  Licensed under the Apache License, Version 2.0 (the "License");
//  you may not use this file except in compliance with the License.
//  You may obtain a copy of the License at
//
//  http://www.apache.org/licenses/LICENSE-2.0
//
//  Unless required by applicable law or agreed to in writing, software
//  distributed under the License is distributed on an "AS IS" BASIS,
//  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
//  See the License for the specific language governing permissions and
//  limitations under the License.
//
//  TermVisitor.h
//

#ifndef TERMVISITOR_H
#define TERMVISITOR_H

#include <deque>
#include <list>
#include <set>

#include "Term.h"

namespace logic {
    using namespace std;
    
    // How do visitors do double-dispatch?
    // Call T.Accept(TV), a virtual method, which dispatches back to
    // TV.Visit(static type).
    // 
    
    // A TermVisitor can be passed to the Term.Accept method, which
    // will invoke TermVisitor.Visit(T) on each subterm of the root Term.
    // If unique is set to true, then the visitor will only visit a
    // given node one time.
    class TermVisitor {
    public:
        enum Order {
            DFS_PREORDER = 0,
            DFS_POSTORDER = 1,
            BFS = 2
        };
        
        TermVisitor(Order ord = DFS_PREORDER, bool uniq = false) : order(ord), unique(uniq) {}
        
        virtual void Visit(Constant *constant) = 0;
        virtual void Visit(Variable *variable) = 0;
        virtual void Visit(Structure *structure) = 0;
        virtual void Visit(Predicate *predicate) = 0;
        
        Order GetOrder() { return order; }
        
        void AddTerm(Term *term);
        
        // Visit the subtree rooted at term.
        void Run(Term *term);
        
    private:
        Order order;
        bool unique;
        deque<Term*> worklist;
        set<Term*> visited;        // Used for unique visitors.
    };
}  // namespace logic

#endif  // TERMVISITOR_H
